0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 169 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 156 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 PiDPToQDPProof (⇒, 14 ms)
↳30 QDP
↳31 Rewriting (⇔, 0 ms)
↳32 QDP
↳33 UsableRulesProof (⇔, 0 ms)
↳34 QDP
↳35 QReductionProof (⇔, 10 ms)
↳36 QDP
↳37 QDPOrderProof (⇔, 127 ms)
↳38 QDP
↳39 DependencyGraphProof (⇔, 0 ms)
↳40 QDP
↳41 UsableRulesProof (⇔, 0 ms)
↳42 QDP
↳43 QReductionProof (⇔, 0 ms)
↳44 QDP
↳45 QDPOrderProof (⇔, 55 ms)
↳46 QDP
↳47 DependencyGraphProof (⇔, 0 ms)
↳48 TRUE
GCDB_IN_GGA(s(X1), s(X2), X3) → U4_GGA(X1, X2, X3, leA_in_gg(X1, X2))
GCDB_IN_GGA(s(X1), s(X2), X3) → LEA_IN_GG(X1, X2)
LEA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, leA_in_gg(X1, X2))
LEA_IN_GG(s(X1), s(X2)) → LEA_IN_GG(X1, X2)
GCDB_IN_GGA(s(X1), s(X2), X3) → U5_GGA(X1, X2, X3, lecA_in_gg(X1, X2))
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → U6_GGA(X1, X2, X3, addE_in_gag(X1, X4, X2))
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → ADDE_IN_GAG(X1, X4, X2)
ADDE_IN_GAG(s(X1), X2, s(X3)) → U2_GAG(X1, X2, X3, addE_in_gag(X1, X2, X3))
ADDE_IN_GAG(s(X1), X2, s(X3)) → ADDE_IN_GAG(X1, X2, X3)
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, X3, addcC_in_gag(X1, X4, X2))
U7_GGA(X1, X2, X3, addcC_out_gag(X1, X4, X2)) → U8_GGA(X1, X2, X3, gcdB_in_gga(s(X1), X4, X3))
U7_GGA(X1, X2, X3, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4, X3)
GCDB_IN_GGA(X1, X2, X3) → U9_GGA(X1, X2, X3, gtD_in_gg(X1, X2))
GCDB_IN_GGA(X1, X2, X3) → GTD_IN_GG(X1, X2)
GTD_IN_GG(s(X1), s(X2)) → U3_GG(X1, X2, gtD_in_gg(X1, X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
GCDB_IN_GGA(X1, s(X2), X3) → U10_GGA(X1, X2, X3, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → U11_GGA(X1, X2, X3, addE_in_gag(s(X2), X4, X1))
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → ADDE_IN_GAG(s(X2), X4, X1)
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, X3, addcE_in_gag(s(X2), X4, X1))
U12_GGA(X1, X2, X3, addcE_out_gag(s(X2), X4, X1)) → U13_GGA(X1, X2, X3, gcdB_in_gga(s(X2), X4, X3))
U12_GGA(X1, X2, X3, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4, X3)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X2, X3) → U25_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(s(X1), X2, s(X3)) → U23_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(0, X1, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
GCDB_IN_GGA(s(X1), s(X2), X3) → U4_GGA(X1, X2, X3, leA_in_gg(X1, X2))
GCDB_IN_GGA(s(X1), s(X2), X3) → LEA_IN_GG(X1, X2)
LEA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, leA_in_gg(X1, X2))
LEA_IN_GG(s(X1), s(X2)) → LEA_IN_GG(X1, X2)
GCDB_IN_GGA(s(X1), s(X2), X3) → U5_GGA(X1, X2, X3, lecA_in_gg(X1, X2))
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → U6_GGA(X1, X2, X3, addE_in_gag(X1, X4, X2))
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → ADDE_IN_GAG(X1, X4, X2)
ADDE_IN_GAG(s(X1), X2, s(X3)) → U2_GAG(X1, X2, X3, addE_in_gag(X1, X2, X3))
ADDE_IN_GAG(s(X1), X2, s(X3)) → ADDE_IN_GAG(X1, X2, X3)
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, X3, addcC_in_gag(X1, X4, X2))
U7_GGA(X1, X2, X3, addcC_out_gag(X1, X4, X2)) → U8_GGA(X1, X2, X3, gcdB_in_gga(s(X1), X4, X3))
U7_GGA(X1, X2, X3, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4, X3)
GCDB_IN_GGA(X1, X2, X3) → U9_GGA(X1, X2, X3, gtD_in_gg(X1, X2))
GCDB_IN_GGA(X1, X2, X3) → GTD_IN_GG(X1, X2)
GTD_IN_GG(s(X1), s(X2)) → U3_GG(X1, X2, gtD_in_gg(X1, X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
GCDB_IN_GGA(X1, s(X2), X3) → U10_GGA(X1, X2, X3, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → U11_GGA(X1, X2, X3, addE_in_gag(s(X2), X4, X1))
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → ADDE_IN_GAG(s(X2), X4, X1)
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, X3, addcE_in_gag(s(X2), X4, X1))
U12_GGA(X1, X2, X3, addcE_out_gag(s(X2), X4, X1)) → U13_GGA(X1, X2, X3, gcdB_in_gga(s(X2), X4, X3))
U12_GGA(X1, X2, X3, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4, X3)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X2, X3) → U25_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(s(X1), X2, s(X3)) → U23_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(0, X1, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X2, X3) → U25_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(s(X1), X2, s(X3)) → U23_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(0, X1, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
ADDE_IN_GAG(s(X1), X2, s(X3)) → ADDE_IN_GAG(X1, X2, X3)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X2, X3) → U25_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(s(X1), X2, s(X3)) → U23_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(0, X1, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
ADDE_IN_GAG(s(X1), X2, s(X3)) → ADDE_IN_GAG(X1, X2, X3)
ADDE_IN_GAG(s(X1), s(X3)) → ADDE_IN_GAG(X1, X3)
From the DPs we obtained the following set of size-change graphs:
LEA_IN_GG(s(X1), s(X2)) → LEA_IN_GG(X1, X2)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X2, X3) → U25_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(s(X1), X2, s(X3)) → U23_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(0, X1, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
LEA_IN_GG(s(X1), s(X2)) → LEA_IN_GG(X1, X2)
LEA_IN_GG(s(X1), s(X2)) → LEA_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
GCDB_IN_GGA(s(X1), s(X2), X3) → U5_GGA(X1, X2, X3, lecA_in_gg(X1, X2))
U5_GGA(X1, X2, X3, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, X3, addcC_in_gag(X1, X4, X2))
U7_GGA(X1, X2, X3, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4, X3)
GCDB_IN_GGA(X1, s(X2), X3) → U10_GGA(X1, X2, X3, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, X3, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, X3, addcE_in_gag(s(X2), X4, X1))
U12_GGA(X1, X2, X3, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4, X3)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X2, X3) → U25_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(s(X1), X2, s(X3)) → U23_gag(X1, X2, X3, addcE_in_gag(X1, X2, X3))
addcE_in_gag(0, X1, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X2, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, addcC_in_gag(X1, X2))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(X1, s(X2)) → U10_GGA(X1, X2, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, addcE_in_gag(s(X2), X1))
U12_GGA(X1, X2, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X3) → U25_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcC_in_gag(x0, x1)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(X1, s(X2)) → U10_GGA(X1, X2, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, addcE_in_gag(s(X2), X1))
U12_GGA(X1, X2, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcC_in_gag(X1, X3) → U25_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcC_in_gag(x0, x1)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(X1, s(X2)) → U10_GGA(X1, X2, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, addcE_in_gag(s(X2), X1))
U12_GGA(X1, X2, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcC_in_gag(x0, x1)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
addcC_in_gag(x0, x1)
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(X1, s(X2)) → U10_GGA(X1, X2, gtcD_in_gg(X1, s(X2)))
U10_GGA(X1, X2, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, addcE_in_gag(s(X2), X1))
U12_GGA(X1, X2, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U10_GGA(X1, X2, gtcD_out_gg(X1, s(X2))) → U12_GGA(X1, X2, addcE_in_gag(s(X2), X1))
POL(0) = 0
POL(GCDB_IN_GGA(x1, x2)) = x1
POL(U10_GGA(x1, x2, x3)) = x3
POL(U12_GGA(x1, x2, x3)) = 1 + x2
POL(U15_gg(x1, x2, x3)) = 0
POL(U23_gag(x1, x2, x3)) = 0
POL(U24_gg(x1, x2, x3)) = 1 + x3
POL(U25_gag(x1, x2, x3)) = 0
POL(U5_GGA(x1, x2, x3)) = 1 + x1
POL(U7_GGA(x1, x2, x3)) = 1 + x1
POL(addcC_out_gag(x1, x2, x3)) = 0
POL(addcE_in_gag(x1, x2)) = 0
POL(addcE_out_gag(x1, x2, x3)) = 0
POL(gtcD_in_gg(x1, x2)) = x1
POL(gtcD_out_gg(x1, x2)) = 1 + x2
POL(lecA_in_gg(x1, x2)) = 0
POL(lecA_out_gg(x1, x2)) = 0
POL(s(x1)) = 1 + x1
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(X1, s(X2)) → U10_GGA(X1, X2, gtcD_in_gg(X1, s(X2)))
U12_GGA(X1, X2, addcE_out_gag(s(X2), X4, X1)) → GCDB_IN_GGA(s(X2), X4)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
gtcD_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U24_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
gtcD_in_gg(x0, x1)
U24_gg(x0, x1, x2)
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GCDB_IN_GGA(s(X1), s(X2)) → U5_GGA(X1, X2, lecA_in_gg(X1, X2))
POL(0) = 0
POL(GCDB_IN_GGA(x1, x2)) = x2
POL(U15_gg(x1, x2, x3)) = 0
POL(U23_gag(x1, x2, x3)) = x3
POL(U25_gag(x1, x2, x3)) = x3
POL(U5_GGA(x1, x2, x3)) = x2
POL(U7_GGA(x1, x2, x3)) = x3
POL(addcC_out_gag(x1, x2, x3)) = x2
POL(addcE_in_gag(x1, x2)) = x2
POL(addcE_out_gag(x1, x2, x3)) = x2
POL(lecA_in_gg(x1, x2)) = 0
POL(lecA_out_gg(x1, x2)) = 0
POL(s(x1)) = 1 + x1
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
U5_GGA(X1, X2, lecA_out_gg(X1, X2)) → U7_GGA(X1, X2, U25_gag(X1, X2, addcE_in_gag(X1, X2)))
U7_GGA(X1, X2, addcC_out_gag(X1, X4, X2)) → GCDB_IN_GGA(s(X1), X4)
lecA_in_gg(s(X1), s(X2)) → U15_gg(X1, X2, lecA_in_gg(X1, X2))
lecA_in_gg(0, s(X1)) → lecA_out_gg(0, s(X1))
lecA_in_gg(0, 0) → lecA_out_gg(0, 0)
U15_gg(X1, X2, lecA_out_gg(X1, X2)) → lecA_out_gg(s(X1), s(X2))
addcE_in_gag(s(X1), s(X3)) → U23_gag(X1, X3, addcE_in_gag(X1, X3))
addcE_in_gag(0, X1) → addcE_out_gag(0, X1, X1)
U25_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcC_out_gag(X1, X2, X3)
U23_gag(X1, X3, addcE_out_gag(X1, X2, X3)) → addcE_out_gag(s(X1), X2, s(X3))
lecA_in_gg(x0, x1)
U15_gg(x0, x1, x2)
addcE_in_gag(x0, x1)
U23_gag(x0, x1, x2)
U25_gag(x0, x1, x2)